(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r0 Real)
(declare-const v7 Bool)
(declare-const r1 Real)
(declare-const v8 Bool)
(declare-const r2 Real)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const v13 Bool)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const v14 Bool)
(declare-const r7 Real)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (or (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r2) v0 (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r1 (- (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2))) (<= r0 (* (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (- (/ r0 r0)) r3) r2) r3) (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0))) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> 0.0 r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 0.0 0.0 (- 0.0)) (+ r2 (- r0 (* (- 0.0) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r1 0.0) (> 0.0 r2 0.0) (or (distinct v7 v1) (<= r1 (- r0 (* 0.0 r1 0.0 r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0))))
(assert (or v2 v0 (>= 0.0 r3 0.0 0.0 r7)))
(assert (or v0 (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r1 0.0) (<= r0 (* (- r0 (* (- 0.0) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (- (/ r0 r0)) r3) r2) r3) (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0))) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r1 (+ r2 0.0 0.0 (+ 0.0 (- 0.0) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2)) (> (/ r0 r0) r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (or (distinct v7 v1) (<= r1 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) 0.0 (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0)) (<= 0.0 0.0 9.232216 (* r0 0.0) (- (- (/ r0 r0))))))
(assert (or (or v10 v13 (xor v13 v14 (<= r0 r0 0.0 r0) (not v10) v15 (= 0.0 r1 0.0) (<= r0 0.0 r3) (distinct 0.0 0.0 0.0)) (> 0.0 r1 r1 r0) v16 (distinct v2 (> 0.0 r1 r1 r0) (distinct v7 v1) v2 (>= r4 0.0 0.0 r1 (+ r2 (- r0 0.0 0.0 (- 0.0)) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2)) (> (/ r0 r0) r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (or (distinct v7 v1) (<= r1 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0 0.0) (distinct v7 v1) (distinct r0 r0) (> (+ 0.0 0.0 r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) 0.0 r2) (<= 0.0 (- r0 (* 0.0 r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)))) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r2) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 9.232216 (* r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- (- (/ r0 r0))))))
(assert (or (>= (- r1) r3 (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (/ r0 r0) r7) (distinct 0.0 r2) (distinct 0.0 r2)))
(assert (or (> (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (> 0.0 (/ 0.0 (* 0.0 r1 0.0 r0 r0))) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) 0.0 9.232216 0.0 0.0)))
(assert (or (>= 0.0 r3 0.0 0.0 r7) (> (+ r2 0.0 0.0 (+ 0.0 0.0 r0 (+ r2 0.0)) r2) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 9.232216 (* r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- (- (/ r0 r0))))))
(assert (or (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= 0.0 r1 0.0) (<= r0 0.0 r3) (distinct 0.0 0.0 0.0)) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* 0.0 r1 (/ r0 r0) r0 r0))) r2) r1 0.0) (> 0.0 r2 0.0) (or (distinct v7 v1) (<= r1 (- r0 (* 0.0 r1 (/ r0 r0) r0 r0) 0.0 (- 0.0))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct 0.0 r0) (and v3 v3 (distinct 0.0 0.0 0.0) v7 v1)) (<= 0.0 (- r0 0.0 0.0 0.0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)))) (distinct 0.0 r2) v2))
(check-sat)
(check-sat)
